es:ES, Cmd, Rsp:Type, isupdate:(Cmd), Delta:(({c:Cmd| (isupdate(c))}  List)Rsp),
Q:(({c:Cmd| (isupdate(c))}  List){c:Cmd| ((isupdate(c)))} Rsp), In:AbsInterface(Cmd),
Out:AbsInterface(Rsp), Sys:AbsInterface(Cmd List), Ack:AbsInterface(), f:sys-antecedent(es;Sys),
g:sys-antecedent(es;Ack).
chain-replication-acks{i:l}
chain-replication-acks(es; Cmd; Rsp; isupdate; In; Out; Sys; Ack; f; g; Delta; Q)
 abstract-chain-replication{i:l}
 abstract-chain-replication(es; Cmd; Rsp; isupdate; In; Out; Sys; f; Delta; Q) 

latex

Up	abstract chain replication
Definitions	f(a), X(e), ||as||, e  X, if b then t else f fi , , s = t, E(X), x:AB(x), es-interface-history(es; X; e), filter(P;l), is-query(In;isupdate;e), A, P  Q, x:A  B(x), P & Q, x:A. B(x), ES, x:A. B(x), Type, AbsInterface(A), sys-antecedent(es;Sys), fifo-antecedent(es;Sys;f), input-forwarding{i:l}(es; Cmd; Sys; isupdate; In; f), loc(e), Id, adjacent(T;L;x;y), chain-consistent(f;chain), p-conditional(f; g), chain-config(es;Sys;chain), type List, b, left + right, P  Q, E, {x:A| B(x)} , P  Q, P  Q, A c B, abstract-chain-replication, chain-replication-acks, t  T, EState(T), a:A fp B(a), , strong-subtype(A;B), EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), !Void(), x:A.B(x), Top, S  T, suptype(S; T), first(e), <a, b>, pred(e), x.A(x), x. t(x), f(x)?z, e c e', Outcome, #$n, A  B, did-forward(es; Sys; f; e), False, e loc e' , hd(l), (x  l), case b of inl(x) => s(x) | inr(y) => t(y), a < b, L1  L2, no_repeats(T;l), (e <loc e'), let x,y = A in B(x;y), t.1, f  g, es-vartype(es; i; x), es-state(es; i), decl-state(ds), ma-state(ds), x  dom(f), {T}, ff, inr x , tt, inl x , True, T, Dec(P), b | a, a ~ b, a  b, a <p b, a < b, x f y, xL. P(x), (xL.P(x)), y is f*(x), r < s, q-rel(r;x), l_disjoint(T;l1;l2), (e < e'), e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a  b, IsIntegDom(r), IsPrimeIdeal(R;P)
Lemmas	squash wf, sq stable from decidable, decidable assert, true wf, false wf, btrue wf, bfalse wf, subtype rel set, es-is-interface wf, l member wf, no repeats wf, sublist wf, es-le wf, es-locl wf, adjacent wf, abstract-chain-replication wf, chain-replication-acks wf, le wf, es-causle wf, sys-antecedent wf, es-interface wf, es-interface-subtype rel, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, EState wf, event system wf, fifo-antecedent wf, es-E wf, iff wf, subtype rel wf, assert wf, input-forwarding wf, not wf, is-query wf, chain-consistent wf, Id wf, es-E-interface wf